{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}
{-# OPTIONS_GHC -Wunused-binds #-}

module Agda.TypeChecking.Serialise.Instances.Common (SerialisedRange(..)) where

import qualified Control.Exception as E
import Control.Monad              ( (<$!>) )
import Control.Monad.IO.Class     ( MonadIO(..) )
import Control.Monad.State        ( runStateT )
import Control.Monad.Reader       ( asks )

import Agda.Syntax.Common
import Agda.Syntax.Builtin
import Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Concrete (RecordDirective(..))
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Position as P
import Agda.Syntax.Literal
import Agda.Syntax.TopLevelModuleName
import Agda.Interaction.FindFile
import Agda.Interaction.Library

import Agda.TypeChecking.Monad.Base.Types
import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances.General ()

import Agda.Utils.FileId (getIdFile)
import Agda.Utils.Null

import Agda.Utils.IORef
import Agda.Utils.Impossible
import Agda.Utils.CallStack
import qualified Agda.Utils.HashTable as H
import qualified Agda.Utils.CompactRegion as Compact

instance EmbPrj ConstructorOrPatternSynonym

instance EmbPrj FileType where
  icod_ AgdaFileType  = pure 0
  icod_ MdFileType    = pure 1
  icod_ RstFileType   = pure 2
  icod_ TexFileType   = pure 3
  icod_ OrgFileType   = pure 4
  icod_ TypstFileType = pure 5
  icod_ TreeFileType  = pure 6

  value = \case
    0 -> pure AgdaFileType
    1 -> pure MdFileType
    2 -> pure RstFileType
    3 -> pure TexFileType
    4 -> pure OrgFileType
    5 -> pure TypstFileType
    6 -> pure TreeFileType
    _ -> malformed

instance EmbPrj Cubical where
  icod_ CWithoutGlue = icodeN'  CWithoutGlue
  icod_ CErased      = icodeN 0 CErased
  icod_ CFull        = icodeN 1 CFull

  value = vcase $ \case
    N0   -> valuN CWithoutGlue
    N1 0 -> valuN CErased
    N1 1 -> valuN CFull
    _    -> malformed

instance EmbPrj Language where
  icod_ WithoutK    = icodeN'  WithoutK
  icod_ WithK       = icodeN 0 WithK
  icod_ (Cubical a) = icodeN 1 Cubical a

  value = vcase $ \case
    N0     -> valuN WithoutK
    N1 0   -> valuN WithK
    N2 1 a -> valuN Cubical a
    _      -> malformed

instance EmbPrj a => EmbPrj (Position' a) where
  icod_ (P.Pn file pos line col) = icodeN' P.Pn file pos line col

  value = valueN P.Pn

instance EmbPrj TopLevelModuleName where
  icod_ (TopLevelModuleName a b c d) = icodeN' TopLevelModuleName a b c d

  value = valueN TopLevelModuleName

instance EmbPrj a => EmbPrj (P.Interval' a) where
  icod_ (P.Interval f p q) = icodeN' P.Interval f p q

  value = valueN P.Interval

instance EmbPrj RangeFile where
  icod_ (RangeFile _ Nothing)  = __IMPOSSIBLE__
  icod_ (RangeFile _ (Just a)) = icode a

  value r = do
    !m :: TopLevelModuleName <- value r
    !mfref    <- asks modFile
    !mf       <- liftIO $ readIORef mfref
    !incs     <- asks includes
    (!r, !mf) <- liftIO $ runStateT (findFile'' incs m) mf
    liftIO $ writeIORef mfref mf
    case r of
      Left err ->
        liftIO $ E.throwIO $ E.ErrorCall $ "file not found: " ++ show err
      Right (SourceFile i) -> do
        let !fp = getIdFile (fileDict mf) i
        !fpmemo <- asks filePathMemo
        !arena  <- asks arena
        liftIO $ H.insertingIfAbsent fpmemo fp
          (\fp -> pure $ RangeFile fp (Just m))
          (Compact.add arena fp)
          (\fp -> pure $ RangeFile fp (Just m))

-- | Ranges are always deserialised as 'noRange'.

instance EmbPrj Range where
  icod_ _ = icodeN' ()
  value _ = return noRange

instance EmbPrj KwRange where
  icod_ _ = icodeN' ()
  value _ = return empty

-- | Ranges that should be serialised properly.

newtype SerialisedRange = SerialisedRange { underlyingRange :: Range }

instance EmbPrj SerialisedRange where
  icod_ (SerialisedRange r) = icodeN' P.intervalsToRange (P.rangeFile r) (P.rangeIntervals r)

  value i = SerialisedRange <$!> valueN P.intervalsToRange i

instance EmbPrj C.Name where
  icod_ (C.NoName a b)     = icodeN 0 C.NoName a b
  icod_ (C.Name r nis xs)  = icodeN 1 C.Name r nis xs

  value = vcase valu where
    valu (N3 0 a b)      = valuN C.NoName a b
    valu (N4 1 r nis xs) = valuN C.Name   r nis xs
    valu _               = malformed

instance EmbPrj NamePart where
  icod_ Hole   = icodeN' Hole
  icod_ (Id a) = icodeN' Id a

  value = vcase valu where
    valu N0     = valuN Hole
    valu (N1 a) = valuN Id a
    valu _      = malformed

instance EmbPrj NameInScope where
  icod_ InScope    = icodeN' InScope
  icod_ NotInScope = icodeN 0 NotInScope

  value = vcase valu where
    valu N0     = valuN InScope
    valu (N1 0) = valuN NotInScope
    valu _      = malformed

instance EmbPrj C.QName where
  icod_ (Qual    a b) = icodeN' Qual a b
  icod_ (C.QName a  ) = icodeN' C.QName a

  value = vcase valu where
    valu (N2 a b) = valuN Qual    a b
    valu (N1 a)   = valuN C.QName a
    valu _        = malformed

instance (EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) where
  icod_ (ImportedModule a) = icodeN 1 ImportedModule a
  icod_ (ImportedName a)   = icodeN 2 ImportedName a

  value = vcase valu where
    valu (N2 1 a) = valuN ImportedModule a
    valu (N2 2 a) = valuN ImportedName a
    valu _ = malformed

instance EmbPrj Associativity where
  icod_ LeftAssoc  = pure 0
  icod_ RightAssoc = pure 1
  icod_ NonAssoc   = pure 2

  value = \case
    0 -> pure LeftAssoc
    1 -> pure RightAssoc
    2 -> pure NonAssoc
    _ -> malformed

instance EmbPrj FixityLevel where
  icod_ Unrelated   = icodeN' Unrelated
  icod_ (Related a) = icodeN' Related a

  value = vcase valu where
    valu N0     = valuN Unrelated
    valu (N1 a) = valuN Related a
    valu _      = malformed

instance EmbPrj Fixity where
  icod_ (Fixity a b c) = icodeN' Fixity a b c

  value = valueN Fixity

instance EmbPrj Fixity' where
  icod_ (Fixity' a b r) = icodeN' (\ a b -> Fixity' a b r) a b  -- discard theNameRange

  value = valueN (\ f n -> Fixity' f n noRange)

instance EmbPrj BoundVariablePosition where
  icod_ (BoundVariablePosition a b) = icodeN' BoundVariablePosition a b

  value = valueN BoundVariablePosition

instance EmbPrj NotationPart where
  icod_ (VarPart a b)  = icodeN 0 VarPart a b
  icod_ (HolePart a b) = icodeN 1 HolePart a b
  icod_ (WildPart a)   = icodeN 2 WildPart a
  icod_ (IdPart a)     = icodeN' IdPart a

  value = vcase valu where
    valu (N3 0 a b) = valuN VarPart a b
    valu (N3 1 a b) = valuN HolePart a b
    valu (N2 2 a)   = valuN WildPart a
    valu (N1 a)     = valuN IdPart a
    valu _          = malformed

instance EmbPrj MetaId where
  icod_ (MetaId a b) = icode (a, b)

  value m = uncurry MetaId <$!> value m

instance EmbPrj ProblemId where
  icod_ (ProblemId a) = icode a

  value m = ProblemId <$!> value m

instance EmbPrj A.QName where
  icod_ n@(A.QName a b) = icodeMemo qnameD qnameC (qnameId n) $ icodeN' A.QName a b

  value = valueN A.QName

instance EmbPrj A.AmbiguousQName where
  icod_ (A.AmbQ a) = icode a
  value n          = A.AmbQ <$!> value n

instance EmbPrj A.ModuleName where
  icod_ (A.MName a) = icode a
  value n           = A.MName <$!> value n

instance EmbPrj A.Name where
  icod_ (A.Name a b c d e f) = icodeMemo nameD nameC a $
    icodeN' (\ a b c d e f -> A.Name a b c (underlyingRange d) e f) a b c (SerialisedRange d) e f

  value = valueN (\a b c d e f -> A.Name a b c (underlyingRange d) e f)

instance EmbPrj a => EmbPrj (C.FieldAssignment' a) where
  icod_ (C.FieldAssignment a b) = icodeN' C.FieldAssignment a b

  value = valueN C.FieldAssignment

instance (EmbPrj s, EmbPrj t) => EmbPrj (Named s t) where
  icod_ (Named a b) = icodeN' Named a b

  value = valueN Named

instance EmbPrj a => EmbPrj (Ranged a) where
  icod_ (Ranged r x) = icodeN' Ranged r x

  value = valueN Ranged

instance EmbPrj ArgInfo where
  icod_ (ArgInfo h r o fv ann) = icodeN' ArgInfo h r o fv ann

  value = valueN ArgInfo

instance EmbPrj ModuleNameHash where
  icod_ (ModuleNameHash a) = icodeN' ModuleNameHash a

  value = valueN ModuleNameHash

instance EmbPrj NameId where
  icod_ (NameId a b) = icodeN' NameId a b

  value = valueN NameId

instance EmbPrj OpaqueId where
  icod_ (OpaqueId a b) = icodeN' OpaqueId a b

  value = valueN OpaqueId

instance EmbPrj a => EmbPrj (WithHiding a) where
  icod_ (WithHiding a b) = icodeN' WithHiding a b

  value = valueN WithHiding

instance EmbPrj a => EmbPrj (Arg a) where
  icod_ (Arg i e) = icodeN' Arg i e

  value = valueN Arg

instance EmbPrj a => EmbPrj (HasEta' a) where
  icod_ YesEta    = icodeN' YesEta
  icod_ (NoEta a) = icodeN' NoEta a

  value = vcase valu where
    valu N0     = valuN YesEta
    valu (N1 a) = valuN NoEta a
    valu _      = malformed

instance EmbPrj PatternOrCopattern

instance EmbPrj a => EmbPrj (DataOrRecord' a) where
  icod_ = \case
    IsData      -> icodeN' IsData
    IsRecord pm -> icodeN' IsRecord pm

  value = vcase $ \case
    N0    -> valuN IsData
    N1 pm -> valuN IsRecord pm
    _     -> malformed

instance EmbPrj OverlapMode

instance EmbPrj Induction where
  icod_ Inductive   = icodeN' Inductive
  icod_ CoInductive = icodeN 1 CoInductive

  value = vcase valu where
    valu N0     = valuN Inductive
    valu (N1 1) = valuN CoInductive
    valu _      = malformed

instance EmbPrj Hiding where
  icod_ Hidden                = return 0
  icod_ NotHidden             = return 1
  icod_ (Instance NoOverlap)  = return 2
  icod_ (Instance YesOverlap) = return 3

  value 0 = return Hidden
  value 1 = return NotHidden
  value 2 = return (Instance NoOverlap)
  value 3 = return (Instance YesOverlap)
  value _ = malformed

instance EmbPrj Q0Origin where
  icod_ = \case
    Q0Inferred -> return 0
    Q0 _       -> return 1
    Q0Erased _ -> return 2

  value = \case
    0 -> return $ Q0Inferred
    1 -> return $ Q0       noRange
    2 -> return $ Q0Erased noRange
    _ -> malformed

instance EmbPrj Q1Origin where
  icod_ = \case
    Q1Inferred -> return 0
    Q1 _       -> return 1
    Q1Linear _ -> return 2

  value = \case
    0 -> return $ Q1Inferred
    1 -> return $ Q1       noRange
    2 -> return $ Q1Linear noRange
    _ -> malformed

instance EmbPrj QωOrigin where
  icod_ = \case
    QωInferred -> return 0
    Qω _       -> return 1
    QωPlenty _ -> return 2

  value = \case
    0 -> return $ QωInferred
    1 -> return $ Qω       noRange
    2 -> return $ QωPlenty noRange
    _ -> malformed

instance EmbPrj Quantity where
  icod_ = \case
    Quantity0 a -> icodeN 0 Quantity0 a
    Quantity1 a -> icodeN 1 Quantity1 a
    Quantityω a -> icodeN'  Quantityω a  -- default quantity, shorter code

  value = vcase $ \case
    (N2 0 a) -> valuN Quantity0 a
    (N2 1 a) -> valuN Quantity1 a
    (N1 a)   -> valuN Quantityω a
    _        -> malformed

-- -- ALT: forget quantity origin when serializing?
-- instance EmbPrj Quantity where
--   icod_ Quantity0 = return 0
--   icod_ Quantity1 = return 1
--   icod_ Quantityω = return 2

--   value 0 = return Quantity0
--   value 1 = return Quantity1
--   value 2 = return Quantityω
--   value _ = malformed

instance EmbPrj Cohesion where
  icod_ Flat       = return 0
  icod_ Continuous = return 1
  icod_ Squash     = return 2

  value 0 = return Flat
  value 1 = return Continuous
  value 2 = return Squash
  value _ = malformed

instance EmbPrj ModalPolarity where
  icod_ UnusedPolarity = return 0
  icod_ StrictlyPositive = return 1
  icod_ Positive = return 2
  icod_ Negative = return 3
  icod_ MixedPolarity = return 4

  value 0 = return UnusedPolarity
  value 1 = return StrictlyPositive
  value 2 = return Positive
  value 3 = return Negative
  value 4 = return MixedPolarity
  value _ = malformed

instance EmbPrj PolarityModality where
  icod_ (PolarityModality p o l) = icod_ (p, o, l)

  value n = do
    (p, o, l) <- polPair
    return $ PolarityModality p o l
    where
      polPair :: R (ModalPolarity, ModalPolarity, ModalPolarity)
      polPair = value n

instance EmbPrj Modality where
  icod_ (Modality a b c d) = icodeN' Modality a b c d

  value = vcase $ \case
    (N4 a b c d) -> valuN Modality a b c d
    _ -> malformed

instance EmbPrj OriginRelevant where
  icod_ = \case
    ORelInferred   -> return 0
    ORelRelevant _ -> return 1

  value = \case
    0 -> return $ ORelInferred
    1 -> return $ ORelRelevant noRange
    _ -> malformed

instance EmbPrj OriginIrrelevant where
  icod_ = \case
    OIrrInferred     -> return 0
    OIrrDot _        -> return 1
    OIrrIrr _        -> return 2
    OIrrIrrelevant _ -> return 3

  value = \case
    0 -> return $ OIrrInferred
    1 -> return $ OIrrDot        noRange
    2 -> return $ OIrrIrr        noRange
    3 -> return $ OIrrIrrelevant noRange
    _ -> malformed

instance EmbPrj OriginShapeIrrelevant where
  icod_ = \case
    OShIrrInferred          -> return 0
    OShIrrDotDot _          -> return 1
    OShIrrShIrr _           -> return 2
    OShIrrShapeIrrelevant _ -> return 3

  value = \case
    0 -> return $ OShIrrInferred
    1 -> return $ OShIrrDotDot          noRange
    2 -> return $ OShIrrShIrr           noRange
    3 -> return $ OShIrrShapeIrrelevant noRange
    _ -> malformed

instance EmbPrj Relevance where
  icod_ = \case
    Relevant   a      -> icodeN' Relevant a
    Irrelevant a      -> icodeN 0 Irrelevant a
    ShapeIrrelevant a -> icodeN 1 ShapeIrrelevant a

  value = vcase \case
    N1 a   -> valuN Relevant a
    N2 0 a -> valuN Irrelevant a
    N2 1 a -> valuN ShapeIrrelevant a
    _      -> malformed

instance EmbPrj Annotation where
  icod_ (Annotation l) = icodeN' Annotation l

  value = valueN Annotation

instance EmbPrj Lock where
  icod_ IsNotLock          = pure 0
  icod_ (IsLock LockOTick) = pure 1
  icod_ (IsLock LockOLock) = pure 2

  value 0 = pure IsNotLock
  value 1 = pure (IsLock LockOTick)
  value 2 = pure (IsLock LockOLock)
  value _ = malformed

instance EmbPrj Origin where
  icod_ UserWritten = return 0
  icod_ Inserted    = return 1
  icod_ Reflected   = return 2
  icod_ CaseSplit   = return 3
  icod_ Substitution = return 4
  icod_ ExpandedPun = return 5
  icod_ Generalization = return 6

  value 0 = return UserWritten
  value 1 = return Inserted
  value 2 = return Reflected
  value 3 = return CaseSplit
  value 4 = return Substitution
  value 5 = return ExpandedPun
  value 6 = return Generalization
  value _ = malformed

instance EmbPrj a => EmbPrj (WithOrigin a) where
  icod_ (WithOrigin a b) = icodeN' WithOrigin a b

  value = valueN WithOrigin

instance EmbPrj FreeVariables where
  icod_ UnknownFVs   = icodeN' UnknownFVs
  icod_ (KnownFVs a) = icodeN' KnownFVs a

  value = vcase valu where
    valu N0     = valuN UnknownFVs
    valu (N1 a) = valuN KnownFVs a
    valu _      = malformed

instance EmbPrj ConOrigin where
  icod_ ConOSystem   = return 0
  icod_ ConOCon      = return 1
  icod_ ConORec      = return 2
  icod_ ConOSplit    = return 3
  icod_ ConORecWhere = return 4

  value 0 = return ConOSystem
  value 1 = return ConOCon
  value 2 = return ConORec
  value 3 = return ConOSplit
  value 4 = return ConORecWhere
  value _ = malformed

instance EmbPrj ProjOrigin where
  icod_ ProjPrefix  = return 0
  icod_ ProjPostfix = return 1
  icod_ ProjSystem  = return 2

  value 0 = return ProjPrefix
  value 1 = return ProjPostfix
  value 2 = return ProjSystem
  value _ = malformed

instance EmbPrj Agda.Syntax.Literal.Literal where
  icod_ (LitNat    a)   = icodeN' LitNat a
  icod_ (LitFloat  a)   = icodeN 1 LitFloat a
  icod_ (LitString a)   = icodeN 2 LitString a
  icod_ (LitChar   a)   = icodeN 3 LitChar a
  icod_ (LitQName  a)   = icodeN 5 LitQName a
  icod_ (LitMeta   a b) = icodeN 6 LitMeta a b
  icod_ (LitWord64 a)   = icodeN 7 LitWord64 a

  value = vcase valu where
    valu (N1 a)     = valuN LitNat    a
    valu (N2 1 a)   = valuN LitFloat  a
    valu (N2 2 a)   = valuN LitString a
    valu (N2 3 a)   = valuN LitChar   a
    valu (N2 5 a)   = valuN LitQName  a
    valu (N3 6 a b) = valuN LitMeta   a b
    valu (N2 7 a)   = valuN LitWord64 a
    valu _          = malformed

instance EmbPrj IsAbstract where
  icod_ AbstractDef = icodeN 0 AbstractDef
  icod_ ConcreteDef = icodeN' ConcreteDef

  value = vcase valu where
    valu (N1 0) = valuN AbstractDef
    valu N0     = valuN ConcreteDef
    valu _      = malformed

instance EmbPrj IsOpaque where
  icod_ (OpaqueDef a)  = icodeN' OpaqueDef a
  icod_ TransparentDef = icodeN' TransparentDef

  value = vcase valu where
    valu (N1 a) = valuN OpaqueDef a
    valu N0     = valuN TransparentDef
    valu _      = malformed

instance EmbPrj SrcLoc where
  icod_ (SrcLoc p m f sl sc el ec) = icodeN' SrcLoc p m f sl sc el ec
  value = valueN SrcLoc

instance EmbPrj CallStack where
  icod_ = icode . getCallStack
  value = (<$!>) fromCallSiteList . value

instance EmbPrj Impossible where
  icod_ (Impossible a)              = icodeN 0 Impossible a
  icod_ (Unreachable a)             = icodeN 1 Unreachable a
  icod_ (ImpMissingDefinitions a b) = icodeN 2 ImpMissingDefinitions a b

  value = vcase valu where
    valu (N2 0 a)   = valuN Impossible  a
    valu (N2 1 a)   = valuN Unreachable a
    valu (N3 2 a b) = valuN ImpMissingDefinitions a b
    valu _          = malformed

instance EmbPrj ExpandedEllipsis where
  icod_ NoEllipsis = icodeN' NoEllipsis
  icod_ (ExpandedEllipsis a b) = icodeN 1 ExpandedEllipsis a b

  value = vcase valu where
    valu N0         = valuN NoEllipsis
    valu (N3 1 a b) = valuN ExpandedEllipsis a b
    valu _          = malformed

instance EmbPrj OptionsPragma where
  icod_ (OptionsPragma a b) = icod_ (a, b)

  value op = uncurry OptionsPragma <$!> value op

instance EmbPrj BuiltinId
instance EmbPrj PrimitiveId

instance EmbPrj SomeBuiltin where
  icod_ (BuiltinName x)   = icodeN 0 BuiltinName x
  icod_ (PrimitiveName x) = icodeN 1 PrimitiveName x

  value = vcase valu where
    valu (N2 0 x) = valuN BuiltinName x
    valu (N2 1 x) = valuN PrimitiveName x
    valu _        = malformed

instance EmbPrj IsInstance where
  icod_ = \case
    InstanceDef a  -> icodeN' InstanceDef a
    NotInstanceDef -> icodeN' NotInstanceDef

  value = vcase \case
    N1 a -> valuN InstanceDef a
    N0   -> valuN NotInstanceDef
    _    -> malformed

instance EmbPrj a => EmbPrj (RecordDirectives' a) where
  icod_ (RecordDirectives a b c d) = icodeN' RecordDirectives a b c d

  value = vcase \case
    N4 a b c d -> valuN RecordDirectives a b c d
    _ -> malformed

instance EmbPrj RecordDirective where
  icod_ = \case
    Constructor a b      -> icodeN 0 Constructor a b
    Eta a                -> icodeN 1 Eta a
    Induction a          -> icodeN 2 Induction a
    PatternOrCopattern a -> icodeN 3 PatternOrCopattern a

  value = vcase \case
    (N3 0 a b) -> valuN Constructor a b
    (N2 1 a)   -> valuN Eta a
    (N2 2 a)   -> valuN Induction a
    (N2 3 a)   -> valuN PatternOrCopattern a
    _ -> malformed

instance EmbPrj Catchall where
  icod_ NoCatchall  = icodeN' NoCatchall
  icod_ (YesCatchall x) = icodeN' YesCatchall x

  value = vcase valu where
    valu N0     = valuN NoCatchall
    valu (N1 x) = valuN YesCatchall x
    valu _      = malformed
